i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
update-spec-decl(upd; ds)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 (k:Knd. 
 (fpf-dom(Kind-deq; k; R-da(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd); i)))
  ((k  ecl-kinds(A))  (k  fpf-domain(da)))) 

latex

Definitions

t  ...$L, x(s), IdLnk, sq_type(T), subtype(S; T), top, False, ff, t.1, Y, reduce(f; k; as), deq-member(eq; x; L), guard(T), R-state-var-init(i; ds; da; x; T; v; ks; tr), if b then t else f fi , fpf-empty, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-machine1{$ecl:ut2}(i; ds; da; A), P  Q, x. t(x), t  T, True, T, prop{i:l}, P  Q, ecl-trans-ks(v), P  Q, P  Q, ecl-machine{$ecl:ut2}(i; ds; da; A; snd; upd), R-da(R; i), mkid{$x:ut2}, fpf-dom(eq; x; f), b, P  Q, Knd, Id, x:A. B(x), A c B, ecl-machine3(ds; da; x; T; ks; a; snd), tt, R-state-var(i; ds; da; x; T; ks; tr), ecl-machine2(i; ds; da; x; T; ks; a; upd), A, decidable(P), ecl-trans-tuple{i:l}(ds; da)

Lemmas

IdLnk sq, lnk wf, lnk-decl-dom2, Knd sq, rcv wf, member-fpf-domain, tagof wf, es-dt-dom, isrcv-implies, lnk-decl-dom-implies, fpf-cap wf, fpf-empty wf, es-dt wf, lnk-decl wf, lsrc wf, subtype-fpf2, ecl-tags wf, R-lnk-tags-da, deq wf, subtype rel list, msg-spec-links wf, idlnk-deq wf, remove-repeats wf, not functionality wrt iff, assert of bnot, eqff to assert, bnot wf, fpf-single-dom, assert-eq-id, eqtt to assert, bool wf, bool sq, bool cases, cons member, ma-valtype wf, fpf-single wf3, eq id wf, fpf-empty-join, assert of bor, bor wf, fpf-single wf, ifthenelse wf, reduce wf, fpf-join-dom-sq, false wf, update-spec-vars wf, R-da-Rall, R-state-var-da-dom, ecl wf, msg-spec wf, update-spec wf, update-spec-decl wf, id-deq wf, Id wf, not wf, fpf wf, ecl-machine wf, Kind-deq wf, Knd wf, decidable equal Kind, decidable l member, or functionality wrt iff, fpf-join-dom, iff transitivity, fpf-compatible-single, R-state-var wf, R-da wf, top wf, fpf-join wf, IdLnk wf, fpf-dom wf, assert wf, implies functionality wrt iff, ecl-trans-tuple wf, ecl-trans wf, fpf-trivial-subtype-top, fpf-domain wf, ecl-kinds-ecl-trans, true wf, squash wf, l member wf